1. Field of the Invention
The present invention relates in general to verifying designs and in particular to reducing resource requirements during verification. Still more particularly, the present invention relates to a system, method and computer program product for predicate selection in bit-level compositional transformations.
2. Description of the Related Art
With the increasing penetration of microprocessor-based systems into every facet of human activity, demands have increased on the microprocessor development and production community to produce systems that are free from data corruption. Microprocessors have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of reliability of calculative results. Whether the impact of errors would be measured in human lives or in mere dollars and cents, consumers of microprocessors have lost tolerance for error-prone results. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable microprocessor results has risen to a mission-critical concern.
Formal and semiformal verification techniques provide powerful tools for discovering errors in verifying the correctness of logic designs. Formal and semiformal verification techniques frequently expose probabilistically uncommon scenarios that may result in a functional design failure. Frequently, formal and semiformal verification techniques provide the opportunity to prove that a design is correct (i.e., that no failing scenario exists).
Unfortunately, formal verification techniques require computational resources which are exponential with respect to the size of the design under test. In particular, many formal analysis techniques require exponential resources with respect to the number of state elements in the design under test. Semi-formal verification techniques leverage formal methods on larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage; generally, coverage decreases as design size increases.
Numerous approaches have thus been proposed to reduce the complexity of a design under verification. For example, bisimulation minimization techniques seek to iteratively collapse equivalent states from the design's state transition representation. While such techniques may yield large reductions in state space, they address a PSPACE-complete problem, and the resulting resource cost may outweigh the savings by the verification framework, when compared to methods such as such as symbolic invariant checking.
Predicate abstraction techniques build an overapproximate abstraction of the design under verification. These approaches first select a set of predicates of the original design, then compute the set of possible transitions between predicate valuations, using the result as the abstracted transition system. This overapproximation often results in spurious property failures, requiring a refinement step which increases the number of predicates in the abstracted system to tighten the overapproximation. For larger control-intensive netlists, the number of refinement steps may become exorbitant. Furthermore, the abstracted system may exceed the complexity of the original netlist because it uses predicates as variables, which may exceed the number of original state and input variables, often degrading to an inconclusive result.
Unfortunately, netlist transformation and abstraction techniques operate on predicates detected at word-level representations. Predicates selected at word-level limit prior-art transformations and do not allow them to detect automatically generated (non-word-level) predicates of good quality. Word-level predicates also limit the ability to iteratively and synergistically apply these transformations under a transformation-based verification framework. What is needed is a method, system and computer program product for predicate selection that operates on bit-level netlists to provide high quality predicates for compositional processing.